Correct-By-Construction Control Synthesis in Model-Based Design of Autonomous Systems

speaker: Ufuk Topcu

abstract: How can we affordably build trustworthy autonomous, networked systems? Partly motivated by this question, I describe a shift from the traditional "design+verify" approach to "specify+synthesize" in model-based engineering. I then discuss our recent results on automated synthesis of correct-by-construction, hierarchical control protocols. These results account for hybrid dynamics that are subject to rich temporal logic specifications and heterogenous uncertainties, and that operate in adversarial environments. They combine ideas from control theory with those from computer science, and exploit underlying system-theoretic interpretations to suppress the inherent computational complexity. The expressivity of the resulting design methodology enables us to formally investigate a number of emerging issues in autonomous, networked systems. I conclude my talk with a brief overview of several such issues from my ongoing projects: (i) compositional synthesis for the so-called fractionated systems; (ii) effects of perception imperfections on protocol synthesis; (iii) interfaces between learning modules and reactive controllers with provable guarantees of correctness; and (iv) human-embedded autonomy.

bio: Ufuk Topcu is a Research Assistant Professor in the Department of Electrical and Systems Engineering at the University of Pennsylvania. He received his Ph.D. from the University of California, Berkeley and was a Postdoctoral Scholar at the California Institute of Technology until 2012. His research is on the analysis, design, and verification of autonomous, networked systems.